Inference at * 2 1 1 1 1 
Iof proof for Lemma less-fast-fib:

.....set predicate..... NILNIL

1. f : 
1. n, a, b:.
1. {m:| 
1. {k:. (a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
2. n : 
  f(n,1,0) = fib(n) 

latex

 by (GenConclAtAddr [2]) 
CollapseTHEN ((Auto) 
CollapseTHEN (Auto')) 

latex

C1: 

C1: 3. v : 
C1: 3. {m:| 
C1: 3. {k:.
C1: 3. {(1 = fib(k))  ((k  0)  (0 = 0))  ((0 < k)  (0 = fib(k - 1)))  (m = fib(n+k))} 
C1: 4. f(n,1,0) = v
C1:   v = fib(n)
C.

Definitions	-n, n - m, Void, #$n, n+m, a < b, x:AB(x), T, True, t  T, A  B, A, False, P  Q, s = t, , x:A. B(x), , {x:A| B(x)} , fib(n), f(a)
Lemmas	nat wf, fib wf, le wf